pre-init-p2(es;i;ds;init;a;p;P)
== pre-init-p(es; i; ds; init; P)
== & @i Precondition for a:Outcome(p) is 
== & @i P:State(ds) 
== & (x:Id. (x  dom(ds))  @i x initially init(x):ds(x)) 

latex

---

clarification:

pre-init-p2(es;i;ds;init;a;p;P)
== pre-init-p(es; i; ds; init; P)
== & pre-p(es;i;ds;a;p;P)
== & (x:Id. (fpf-dom(IdDeq; x; ds))  init-p(es; i; dsIdDeq(x); x; initIdDeq(x))) 

latex

Definitions	pre-init-p(es; i; ds; init; P), P & Q, @i Precondition for a:Outcome(p) is P:State(ds) , x:A. B(x), Id, P  Q, b, x  dom(f), @i x initially v:T, f(x), IdDeq
FDL editor aliases	pre-init-p2